\begin{tabbing}
$\forall$\=${\it es}$:ES, $T$:Type, ${\it eq}$:EqDecider($T$), $v$:$T$, $x$:Id, $e$:\{$e$:E$\mid$ @loc($e$)($x$:$T$)\} ,\+
\\[0ex]${\it e'}$:\{${\it e'}$:E$\mid$ $e$ $\leq$loc ${\it e'}$  \& ($x$ after ${\it e'}$) = $v$\} .
\-\\[0ex]next event in [$e$;${\it e'}$] after which $x$ = $v$ $\in$ E
\end{tabbing}